Nuprl Lemma : es-valtype-kindtype
0,22
postcript
pdf
es
,
e
:Top. valtype(
e
) ~ kindtype(loc(
e
);kind(
e
))
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Top
,
valtype(
e
)
,
kindtype(
i
;
k
)
,
isrcv(
e
)
,
rcvtype(
e
)
,
acttype(
e
)
,
lnk(
e
)
,
tag(
e
)
,
act(
e
)
Lemmas
top
wf
origin
es, e:Top. valtype(e) ~ kindtype(loc(e);kind(e)) es, e:Top. valtype(e) ~ kindtype(loc(e);kind(e)) x:A. B(x)
T